YES(O(1),O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ f(nil()) -> nil()
, f(.(nil(), y)) -> .(nil(), f(y))
, f(.(.(x, y), z)) -> f(.(x, .(y, z)))
, g(nil()) -> nil()
, g(.(x, nil())) -> .(g(x), nil())
, g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { g(nil()) -> nil() }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[f](x1) = [1] x1 + [0]
[nil] = [0]
[.](x1, x2) = [1] x1 + [1] x2 + [0]
[g](x1) = [1] x1 + [1]
This order satisfies the following ordering constraints:
[f(nil())] = [0]
>= [0]
= [nil()]
[f(.(nil(), y))] = [1] y + [0]
>= [1] y + [0]
= [.(nil(), f(y))]
[f(.(.(x, y), z))] = [1] y + [1] x + [1] z + [0]
>= [1] y + [1] x + [1] z + [0]
= [f(.(x, .(y, z)))]
[g(nil())] = [1]
> [0]
= [nil()]
[g(.(x, nil()))] = [1] x + [1]
>= [1] x + [1]
= [.(g(x), nil())]
[g(.(x, .(y, z)))] = [1] y + [1] x + [1] z + [1]
>= [1] y + [1] x + [1] z + [1]
= [g(.(.(x, y), z))]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ f(nil()) -> nil()
, f(.(nil(), y)) -> .(nil(), f(y))
, f(.(.(x, y), z)) -> f(.(x, .(y, z)))
, g(.(x, nil())) -> .(g(x), nil())
, g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Weak Trs: { g(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { f(nil()) -> nil() }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[f](x1) = [1] x1 + [2]
[nil] = [2]
[.](x1, x2) = [1] x1 + [1] x2 + [1]
[g](x1) = [1] x1 + [2]
This order satisfies the following ordering constraints:
[f(nil())] = [4]
> [2]
= [nil()]
[f(.(nil(), y))] = [1] y + [5]
>= [1] y + [5]
= [.(nil(), f(y))]
[f(.(.(x, y), z))] = [1] y + [1] x + [1] z + [4]
>= [1] y + [1] x + [1] z + [4]
= [f(.(x, .(y, z)))]
[g(nil())] = [4]
> [2]
= [nil()]
[g(.(x, nil()))] = [1] x + [5]
>= [1] x + [5]
= [.(g(x), nil())]
[g(.(x, .(y, z)))] = [1] y + [1] x + [1] z + [4]
>= [1] y + [1] x + [1] z + [4]
= [g(.(.(x, y), z))]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ f(.(nil(), y)) -> .(nil(), f(y))
, f(.(.(x, y), z)) -> f(.(x, .(y, z)))
, g(.(x, nil())) -> .(g(x), nil())
, g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Weak Trs:
{ f(nil()) -> nil()
, g(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { g(.(x, nil())) -> .(g(x), nil()) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[f](x1) = [1] x1 + [0]
[nil] = [1]
[.](x1, x2) = [1] x1 + [1] x2 + [0]
[g](x1) = [2] x1 + [2]
This order satisfies the following ordering constraints:
[f(nil())] = [1]
>= [1]
= [nil()]
[f(.(nil(), y))] = [1] y + [1]
>= [1] y + [1]
= [.(nil(), f(y))]
[f(.(.(x, y), z))] = [1] y + [1] x + [1] z + [0]
>= [1] y + [1] x + [1] z + [0]
= [f(.(x, .(y, z)))]
[g(nil())] = [4]
> [1]
= [nil()]
[g(.(x, nil()))] = [2] x + [4]
> [2] x + [3]
= [.(g(x), nil())]
[g(.(x, .(y, z)))] = [2] y + [2] x + [2] z + [2]
>= [2] y + [2] x + [2] z + [2]
= [g(.(.(x, y), z))]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ f(.(nil(), y)) -> .(nil(), f(y))
, f(.(.(x, y), z)) -> f(.(x, .(y, z)))
, g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Weak Trs:
{ f(nil()) -> nil()
, g(nil()) -> nil()
, g(.(x, nil())) -> .(g(x), nil()) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { f(.(nil(), y)) -> .(nil(), f(y)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[f](x1) = [2] x1 + [0]
[nil] = [2]
[.](x1, x2) = [1] x1 + [1] x2 + [0]
[g](x1) = [2] x1 + [0]
This order satisfies the following ordering constraints:
[f(nil())] = [4]
> [2]
= [nil()]
[f(.(nil(), y))] = [2] y + [4]
> [2] y + [2]
= [.(nil(), f(y))]
[f(.(.(x, y), z))] = [2] y + [2] x + [2] z + [0]
>= [2] y + [2] x + [2] z + [0]
= [f(.(x, .(y, z)))]
[g(nil())] = [4]
> [2]
= [nil()]
[g(.(x, nil()))] = [2] x + [4]
> [2] x + [2]
= [.(g(x), nil())]
[g(.(x, .(y, z)))] = [2] y + [2] x + [2] z + [0]
>= [2] y + [2] x + [2] z + [0]
= [g(.(.(x, y), z))]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ f(.(.(x, y), z)) -> f(.(x, .(y, z)))
, g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Weak Trs:
{ f(nil()) -> nil()
, f(.(nil(), y)) -> .(nil(), f(y))
, g(nil()) -> nil()
, g(.(x, nil())) -> .(g(x), nil()) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
Trs: { g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[f](x1) = [1 1] x1 + [0]
[0 0] [1]
[nil] = [0]
[0]
[.](x1, x2) = [1 0] x1 + [1 1] x2 + [0]
[0 1] [0 0] [1]
[g](x1) = [2 0] x1 + [2]
[2 1] [0]
This order satisfies the following ordering constraints:
[f(nil())] = [0]
[1]
>= [0]
[0]
= [nil()]
[f(.(nil(), y))] = [1 1] y + [1]
[0 0] [1]
>= [1 1] y + [1]
[0 0] [1]
= [.(nil(), f(y))]
[f(.(.(x, y), z))] = [1 1] y + [1 1] x + [1 1] z + [2]
[0 0] [0 0] [0 0] [1]
>= [1 1] y + [1 1] x + [1 1] z + [2]
[0 0] [0 0] [0 0] [1]
= [f(.(x, .(y, z)))]
[g(nil())] = [2]
[0]
> [0]
[0]
= [nil()]
[g(.(x, nil()))] = [2 0] x + [2]
[2 1] [1]
>= [2 0] x + [2]
[2 1] [1]
= [.(g(x), nil())]
[g(.(x, .(y, z)))] = [2 2] y + [2 0] x + [2 2] z + [4]
[2 2] [2 1] [2 2] [3]
> [2 2] y + [2 0] x + [2 2] z + [2]
[2 2] [2 1] [2 2] [2]
= [g(.(.(x, y), z))]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs: { f(.(.(x, y), z)) -> f(.(x, .(y, z))) }
Weak Trs:
{ f(nil()) -> nil()
, f(.(nil(), y)) -> .(nil(), f(y))
, g(nil()) -> nil()
, g(.(x, nil())) -> .(g(x), nil())
, g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
Trs: { f(.(.(x, y), z)) -> f(.(x, .(y, z))) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[f](x1) = [2 0] x1 + [0]
[1 0] [3]
[nil] = [2]
[0]
[.](x1, x2) = [1 2] x1 + [1 0] x2 + [0]
[0 0] [0 1] [1]
[g](x1) = [1 2] x1 + [0]
[0 0] [1]
This order satisfies the following ordering constraints:
[f(nil())] = [4]
[5]
> [2]
[0]
= [nil()]
[f(.(nil(), y))] = [2 0] y + [4]
[1 0] [5]
> [2 0] y + [2]
[1 0] [4]
= [.(nil(), f(y))]
[f(.(.(x, y), z))] = [2 4] y + [2 4] x + [2 0] z + [4]
[1 2] [1 2] [1 0] [5]
> [2 4] y + [2 4] x + [2 0] z + [0]
[1 2] [1 2] [1 0] [3]
= [f(.(x, .(y, z)))]
[g(nil())] = [2]
[1]
>= [2]
[0]
= [nil()]
[g(.(x, nil()))] = [1 2] x + [4]
[0 0] [1]
>= [1 2] x + [4]
[0 0] [1]
= [.(g(x), nil())]
[g(.(x, .(y, z)))] = [1 2] y + [1 2] x + [1 2] z + [4]
[0 0] [0 0] [0 0] [1]
>= [1 2] y + [1 2] x + [1 2] z + [4]
[0 0] [0 0] [0 0] [1]
= [g(.(.(x, y), z))]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ f(nil()) -> nil()
, f(.(nil(), y)) -> .(nil(), f(y))
, f(.(.(x, y), z)) -> f(.(x, .(y, z)))
, g(nil()) -> nil()
, g(.(x, nil())) -> .(g(x), nil())
, g(.(x, .(y, z))) -> g(.(.(x, y), z)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^1))